<html>
<head>
<title>package alloy.semantic</title>
</head>
<body>
<p>  This package contains the code for doing all semantic checks on a properly
parsed Alloy model.  The checks run on the AST.  These checks are currently
done by AlloyRunner#_performSemanticChecks.  In addition to checking various
properties, the code in this class computes some auxiliary information & fills
in some fields of the nodes of the formula.

<h2>Order of checks</h2>
<pre>
1. Create module scopes by applying a MakeModuleScopesVisitor.  This creates
   the name lookup tables for the paragraphs in each module, and builds a
   mapping from field names to all signatures which declare a field of that
   name.  Creates ModuleScopeTable, which maps module names to ModuleScope's.

catches
- two paragraphs with identical qualified names

2. Apply a NoParagraphNameShadowingVisitor to ensure that no field, type
   parameter, function argument, or qualified variable shadows a paragraph
   name.  This restriction is needed to make parsing work (function names and
   signature names used to disambiguate certain cases in parsing).  Does not
   write anything, just prints error messages.

catches
- shadowing of paragraph name

3. Construct BasicType's for all signatures in the spec.  This involves the
   following steps:

3a. Apply a ConstructExtendsGraphVisitor to construct a graph (should be a DAG) of the extension
   hierarchy of the signatures and check its validity.  This graph is available from the
   visitor through the method getSortedSigs(), which returns a list of the signatures
   topologically sorted so that no signature appears before a signature it extends. 

catches
- duplicate extension of signature (ie. sig A extends B, B {})
- cycle in extends graph (ie. sig A extends A {})
- extension of non-existent signature or non-signature

3b. Create the signature types by calling SigTypeCreator.createSigTypes(), with
   the sorted ArrayList of signatures from the previous step as the argument.  This
   pass creates all necessary BasicType's and associates with each signature a 
   BasicType.  Handles both polymorphic and non-polymorphic sigs.  

catches
- extension of instantiation (eg. sig A {} sig B[t] {} sig C extends B[A] {} )
- duplicate type parameter name in signature (eg. sig A[t,t])
- adding type parameters in extension (eg. sig A[s,t] extends B[t] {} )
- changing order of type parameters in extension (eg. sig A[s,t] extends B[t,s] {})
- extending signatures with different types (eg. sig A {} sig B {} sig C extends A,B {})
- extending two levels of signature hierarchy
  (eg. sig A {} sig B ext A {} sig C ext A, B {} )
  (but the following is legal: sig A {} sig B ext A {} sig C ext A {} sig D ext B,C {} )

4. Given BasicType's for each signature, typecheck the rest of the specification.  Note
   that the "with" construct is also desugared in this step.
   This is done in three steps.

4a. Type check the fields by calling FieldTypeChecker.typecheckFields() on the
    same topologically sorted signature list.  This ordering is important to 
    typecheck cases like sig A { f: A } sig B ext A { f2: f }, the cases in
    which fields of a super-signature are used to declare fields of a 
    sub-signature.  Uses ExprTypeCheckVisitor to type check each field.

catches
- duplicate field in two sigs of the same type (eg. sig A { f: A } sig B ext A { f: B })
- field shadowing type parameter (eg. sig A[t] { t: A[t] } )
- invocation in field declaration

4b. Type check the function formal arguments by applying a FunctionArgTypeCheckVisitor
   to the spec, which in turn uses an ExprTypeCheckVisitor to typecheck each formal.

catches
- invocation in function argument
- duplicate type parameter for function (eg. fun f [t,t] (s: t) {} )
- duplicate function argument

8. Finally, type check the formulas in each formula paragraph (fuctions, facts,
   assertions) by applying a FormulaTypeCheckVisitor to the spec, which in turn
   uses an ExprTypeCheckVisitor to typecheck each formula.

catches
- duplicate type parameter for fact / assertion (eg. assert [t,t] { ... } )
- rightmost basic type of with prefix expression not a SigType
   (eg. fact [t] { with t | ... } since here t has VarType, IntType is also a problem
    because it does not have fields)
- conflict in types of with prefix expressions
   (eg. some x: A, y:A | with x,y | ... )
- two possible with prefix expressions for identifier in body of with
   (eg. sig A { f: A} sig B { f: B } ... all x:A, y: B | with x,y | some f )
- all expression type errors (eg. join of incompatible types)
- duplicate declaration of variable in single scope (eg. all x: A, x: B | ... ),
  although shadowing *is* allowed in a deeper scope
- invocation of non-existent function
- use of non-existent field
- improper instantiations of polymorphic sigs
  - mix of type parameters and sig types (sig A[s,t] {} sig B {} fact [u] { some A[B,u] | ... }
  - instantiation of non-signature

Note that all of these passes assume that the previous passes have completed
successfully.  To ensure that a pass has completed successfully, just check
that alloy.util.Dbg.userError is false after the pass.  Be sure to check this
flag between each pass.  

Also, semantic checks are performed on commands using CommandVisitor.  However,
these checks are currently performed after invocations are inlined (can't remember
why).  

catches
- running a non-function or checking a non-assertion
- running a non-existent function or checking a non-existent assertion
- not specifying a scope for a basic type 
- duplicate specification of scope for a type
- specifying a scope for a non-existent basic type
- specifying a scope for a non-signature name

Note that right now, the width of an Int is specified as the scope of an
imaginary basic type "int".

------------------------------------------------------------------------------

Semantic Checks Performed
-------------------------
Here is a list of semantic checks and the module in which they are performed.

- non-unique unqualified names in module caught in whichever stage detects
that the name is actually used


ConstructExtendsGraphVisitor
----------------------------

NoParagraphNameShadowingVisitor
-------------------------------

SigTypeCreator
--------------

FieldTypeChecker
----------------

FunctionArgTypeCheckVisitor
---------------------------

FormulaTypeCheckVisitor
-----------------------

ExprTypeCheckVisitor
--------------------

------------------------------------------------------------------------------

Naming
------
The classes ModuleScope and LocalScope are primarily used for handling naming.
ModuleScope contains mappings from qualified and unqualified names to
paragraphs for each module.  The Singleton class ModuleScopeTable maps module
names to the corresponding ModuleScope object.  Each ModuleScope also maps
field names to the signatures which contain a field of that name, used for
desugaring with and typechecking transpose operators.

Each LocalScope has a mapping from String names to the RelationType associated
with that name in the scope.  A LocalScope also has a list of parents.
LocalScopes are utilized as follows.  Each signature has two LocalScopes
associated with it, one for its type parameters and a parent LocalScope for its
fields.  We use separate LocalScopes for fields and type parameters since
fields from super sigs should be visible from sub signatures, but type
parameters from super sigs are not visible.  So, the parents of the LocalScope
holding the fields of a signature are the LocalScopes holding the fields of its
super signatures.  Each formula paragraph has a LocalScope binding its type
parameters to VarTypes.  A function also binds its arguments to the appropriate
types in its LocalScope.  Whenever a quantified formula or comprehension
expression is encountered while typechecking a formula, a new LocalScope is
created whose parent is the LocalScope of the enclosing formula / construct.  

Lookup of variables then proceeds as follows.  First, a lookup is performed in
the current LocalScope (which includes a lookup in all of the LocalScope's
ancestors).  If no entry is found, we try to prefix the variable with any
candidate with prefix expressions.  If this also does not work but a type hint
is present, we attempt to type the variable using the hint.  If the hint is a
left type hint, we see if any signature with that left type has a field with
the name of the variable, and if so give the variable the type of the field.
We do the field lookup by starting at the signature corresponding to the type
and looking at its fields, then the fields of its subsigs, etc.  If the hint is
a right type hint, we look up all the signatures which have a field with the
same name as the variable, and see if any of the fields have a second type
matching the hint.  If none if these methods unambiguously types the variable,
we give up.
</pre>
</body>
</html>
  

